module Checker where
-- A consistency checker for first order logic.
-- check returns true if the set of formulas is consistent
-- Written by Patrick Robotham 2011

data WFF = Predicate Predicate [Var] | Conj WFF WFF |
              Disj WFF WFF | Neg WFF | Exists Var WFF |
              Forall Var WFF | T | F 
            deriving (Show, Eq)
                             
-- Should add support for implication, xor, nand, nor 
-- Also for identity, functions

data World = World Freevars Simples Gensym

type Freevars  = [Var]
type Simples   = [WFF]
type Gensym   = Var

type Predicate = String
type Var  = Integer  
-- variables are single characters, converted in to unicode
-- We use extra numbers for gensyms.

testworld = World [] [] gensym

gensym :: Var
gensym = 1024
-- does unicode begin at 1024? Rewrite.


appears :: Var -> WFF -> Bool
-- returns true iff Var appears in the WFF as a free variable
appears c T = False
appears c F = False
appears c (Predicate p xs) = elem c xs
appears c (Conj a b)     = appears c a || appears c b
appears c (Disj a b)     = appears c a || appears c b
appears c (Neg a)        = appears c a
appears c (Exists x wff)  = not (x == c) &&  appears c wff 
appears c (Forall x wff) = not (x == c) &&  appears c wff


--toprenex :: WFF -> WFF
--toprenex p@(Predicate _ _) = p
--toprenex (Conj (Exists a phi) psi =
--           if appears a psi
--           then 

--sigma1 :: WFF -> Bool

--freevars :: WFF -> [Var]










check :: [WFF] -> World -> Bool
-- Returns false if the list of FOLWFFs is inconsistent.
-- It's assumed [Variable] has all free variables in [FOLWFF]
-- It's assumed [FOLWFF] only contains formulas of prenex-0
-- It's assumed [FOLWFF] is in prenex normal form
-- Could refactor to use "case"

check (p@(Predicate _ _):xs) (World free sims n) = 
  check xs (World free (p:sims) n)
check (T:xs) (World free sims n) = check xs (World free (T:sims) n)
check (F:xs) (World free sims n) = check xs (World free (F:sims) n)
check ((Conj x y):xs) w = check (x:y:xs) w
check ((Disj x y):xs) w = check (x:xs) w || check (y:xs) w
check ((Neg (Disj x y)):xs) w = check ((Neg x):(Neg y):xs) w 
check ((Neg (Conj x y)):xs) w = check ((Disj (Neg x) (Neg y)):xs) w
check ((Neg (Neg x)):xs) w    = check (x:xs) w
check (p@(Neg (Predicate _ _)):xs) (World free sims n) = 
  check xs (World free (p:sims) n)
check ((Neg T):xs) (World free sims n) =    
  check xs (World free (F:sims) n)
check ((Neg F):xs) (World free sims n) =
  check xs (World free (T:sims) n)
check ((Neg _):xs) w = error "Not in Prenex normal form!"
check ((Exists var wff):xs) w@(World free sims n) = 
  check ((existinst (Exists var wff) w):xs) (World (n:free) sims (n+1))
check wffs@((Forall var wff):xs) w = 
  if all univ xs
  then let formulas = foldr (++) [] (map (univinstantiate w) wffs) 
       in check formulas w
  else check (xs ++ [(Forall var wff)]) w
check [] w = trivialcheck w
                           

trivialcheck :: World -> Bool
trivialcheck (World _ sims _) 
  | any (== F) sims = False 
  | otherwise =  let negs = [wff | wff <- sims, isneg wff]
                     pos  = [wff | wff <- sims, not (isneg wff)] 
                 in
                  foldr (&&) True (map (\x -> not (elem (Neg x) negs)) pos)   
                  

univ:: WFF -> Bool
univ (Forall _ _) = True
univ _            = False

isneg :: WFF -> Bool
isneg (Neg _) = True
isneg _       = False

univinstantiate:: World -> WFF -> [WFF]
univinstantiate (World free _ _) (Forall a wff) = 
  map inst free
    where inst :: Var -> WFF
          inst var = subst a var  wff 



existinst:: WFF -> World -> WFF
existinst (Exists a wff) (World _ _ n) =
  subst a n wff


subst :: Var -> Var -> WFF -> WFF
-- turns all free variables a in to b in a well formed formula
subst _ _ T = T
subst _ _ F = F
subst a b (Predicate p xs) = 
  Predicate p (map (\x -> if (x == a) then b else x) xs)
subst a b (Conj x y) = Conj (subst a b x) (subst a b y)  
subst a b (Disj x y) = Disj (subst a b x) (subst a b y)
subst a b (Neg x)    = Neg (subst a b x)
subst a b (Exists n x) = if (n == a)
                         then (Exists n  x)
                         else (Exists n (subst a b x))
subst a b (Forall n x) = if (n == a)
                         then (Forall n x)    
                         else (Forall n (subst a b x))
                               


             
                  
                  


